Nuprl Lemma : rng_plus_assoc 13,42

r:Rng, abc:|r|. (a +r (b +r c)) = ((a +r b) +r c |r
latex


Uprings 1
Definitions of StatementRng, r+gp
Definitionst  T, IMonoid, x f y, x:AB(x), t.2, t.1, , P & Q, Mon, Group{i}, r+gp, *, |g|
Lemmasrng wf, grp wf, grp id wf, grp op wf, grp car wf, monoid p wf, add grp of rng wf a, mon assoc

origin